Nuprl Lemma : R-has-loc-base 11,40

R:es_realizer{i:l}, i:Id.
((Rplus?(R)))  ((Rnone?(R)))  (R-has-loc(Ri) = eq_id(R-loc(R); i 
latex


DefinitionsTrue, if b then t else f fi , tt, ff, xt(x), t  T, R-loc(R), R-has-loc(Ri), Rnone?(x1), Rplus?(x1), b, P  Q, x:AB(x), False, x(s), Unit, A, es_realizer{i:l}, Rrframe(locxL), Rbframe(lockL), Raframe(lockL), Rpre(locdsapP), Rsends(dskndTldtg), Reffect(locdskndTxf), Rsframe(lnktagL), Rframe(locTxL), Rinit(locTxv), Rplus(leftright), prop{i:l}, Rnone,
Lemmases realizer wf, lsrc wf, eq id wf, false wf, true wf, not wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf

origin